(set-logic QF_LIA)
(set-info :source |
Mathsat benchmarks available from http://mathsat.itc.it

This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun arg1 () Int)
(declare-fun ARG2_LSBRCK_0_RSBRCK_ () Bool)
(declare-fun arg2_LSBRCK_0_RSBRCK_ () Int)
(declare-fun ARG2_LSBRCK_10_RSBRCK_ () Bool)
(declare-fun arg2_LSBRCK_10_RSBRCK_ () Int)
(declare-fun ARG2_LSBRCK_11_RSBRCK_ () Bool)
(declare-fun arg2_LSBRCK_11_RSBRCK_ () Int)
(declare-fun ARG2_LSBRCK_12_RSBRCK_ () Bool)
(declare-fun arg2_LSBRCK_12_RSBRCK_ () Int)
(declare-fun ARG2_LSBRCK_13_RSBRCK_ () Bool)
(declare-fun arg2_LSBRCK_13_RSBRCK_ () Int)
(declare-fun ARG2_LSBRCK_14_RSBRCK_ () Bool)
(declare-fun arg2_LSBRCK_14_RSBRCK_ () Int)
(declare-fun ARG2_LSBRCK_15_RSBRCK_ () Bool)
(declare-fun arg2_LSBRCK_15_RSBRCK_ () Int)
(declare-fun ARG2_LSBRCK_1_RSBRCK_ () Bool)
(declare-fun arg2_LSBRCK_1_RSBRCK_ () Int)
(declare-fun ARG2_LSBRCK_2_RSBRCK_ () Bool)
(declare-fun arg2_LSBRCK_2_RSBRCK_ () Int)
(declare-fun ARG2_LSBRCK_3_RSBRCK_ () Bool)
(declare-fun arg2_LSBRCK_3_RSBRCK_ () Int)
(declare-fun ARG2_LSBRCK_4_RSBRCK_ () Bool)
(declare-fun arg2_LSBRCK_4_RSBRCK_ () Int)
(declare-fun ARG2_LSBRCK_5_RSBRCK_ () Bool)
(declare-fun arg2_LSBRCK_5_RSBRCK_ () Int)
(declare-fun ARG2_LSBRCK_6_RSBRCK_ () Bool)
(declare-fun arg2_LSBRCK_6_RSBRCK_ () Int)
(declare-fun ARG2_LSBRCK_7_RSBRCK_ () Bool)
(declare-fun arg2_LSBRCK_7_RSBRCK_ () Int)
(declare-fun ARG2_LSBRCK_8_RSBRCK_ () Bool)
(declare-fun arg2_LSBRCK_8_RSBRCK_ () Int)
(declare-fun ARG2_LSBRCK_9_RSBRCK_ () Bool)
(declare-fun arg2_LSBRCK_9_RSBRCK_ () Int)
(declare-fun arg2 () Int)
(declare-fun mul () Int)
(declare-fun mul_sum_LSBRCK_0_RSBRCK_ () Int)
(declare-fun mul_sum_LSBRCK_10_RSBRCK_ () Int)
(declare-fun mul_sum_LSBRCK_11_RSBRCK_ () Int)
(declare-fun mul_sum_LSBRCK_12_RSBRCK_ () Int)
(declare-fun mul_sum_LSBRCK_13_RSBRCK_ () Int)
(declare-fun mul_sum_LSBRCK_14_RSBRCK_ () Int)
(declare-fun mul_sum_LSBRCK_15_RSBRCK_ () Int)
(declare-fun mul_sum_LSBRCK_1_RSBRCK_ () Int)
(declare-fun mul_sum_LSBRCK_2_RSBRCK_ () Int)
(declare-fun mul_sum_LSBRCK_3_RSBRCK_ () Int)
(declare-fun mul_sum_LSBRCK_4_RSBRCK_ () Int)
(declare-fun mul_sum_LSBRCK_5_RSBRCK_ () Int)
(declare-fun mul_sum_LSBRCK_6_RSBRCK_ () Int)
(declare-fun mul_sum_LSBRCK_7_RSBRCK_ () Int)
(declare-fun mul_sum_LSBRCK_8_RSBRCK_ () Int)
(declare-fun mul_sum_LSBRCK_9_RSBRCK_ () Int)
(declare-fun mul_sum () Int)
(assert (let ((?v_0 (not ARG2_LSBRCK_0_RSBRCK_)) (?v_1 (not ARG2_LSBRCK_1_RSBRCK_)) (?v_2 (not ARG2_LSBRCK_2_RSBRCK_)) (?v_3 (not ARG2_LSBRCK_3_RSBRCK_)) (?v_4 (not ARG2_LSBRCK_4_RSBRCK_)) (?v_5 (not ARG2_LSBRCK_5_RSBRCK_)) (?v_6 (not ARG2_LSBRCK_6_RSBRCK_)) (?v_7 (not ARG2_LSBRCK_7_RSBRCK_)) (?v_8 (not ARG2_LSBRCK_8_RSBRCK_)) (?v_9 (not ARG2_LSBRCK_9_RSBRCK_)) (?v_10 (not ARG2_LSBRCK_10_RSBRCK_)) (?v_11 (not ARG2_LSBRCK_11_RSBRCK_)) (?v_12 (not ARG2_LSBRCK_12_RSBRCK_)) (?v_13 (not ARG2_LSBRCK_13_RSBRCK_)) (?v_14 (not ARG2_LSBRCK_14_RSBRCK_)) (?v_15 (not ARG2_LSBRCK_15_RSBRCK_))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= arg2 0) (<= arg2 65535)) (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- arg2 arg2_LSBRCK_0_RSBRCK_) (* 2 arg2_LSBRCK_1_RSBRCK_)) (* 4 arg2_LSBRCK_2_RSBRCK_)) (* 8 arg2_LSBRCK_3_RSBRCK_)) (* 16 arg2_LSBRCK_4_RSBRCK_)) (* 32 arg2_LSBRCK_5_RSBRCK_)) (* 64 arg2_LSBRCK_6_RSBRCK_)) (* 128 arg2_LSBRCK_7_RSBRCK_)) (* 256 arg2_LSBRCK_8_RSBRCK_)) (* 512 arg2_LSBRCK_9_RSBRCK_)) (* 1024 arg2_LSBRCK_10_RSBRCK_)) (* 2048 arg2_LSBRCK_11_RSBRCK_)) (* 4096 arg2_LSBRCK_12_RSBRCK_)) (* 8192 arg2_LSBRCK_13_RSBRCK_)) (* 16384 arg2_LSBRCK_14_RSBRCK_)) (* 32768 arg2_LSBRCK_15_RSBRCK_)) 0)) (>= arg2_LSBRCK_0_RSBRCK_ 0)) (<= arg2_LSBRCK_0_RSBRCK_ 1)) (or ?v_0 (= arg2_LSBRCK_0_RSBRCK_ 1))) (or ARG2_LSBRCK_0_RSBRCK_ (= arg2_LSBRCK_0_RSBRCK_ 0))) (>= arg2_LSBRCK_1_RSBRCK_ 0)) (<= arg2_LSBRCK_1_RSBRCK_ 1)) (or ?v_1 (= arg2_LSBRCK_1_RSBRCK_ 1))) (or ARG2_LSBRCK_1_RSBRCK_ (= arg2_LSBRCK_1_RSBRCK_ 0))) (>= arg2_LSBRCK_2_RSBRCK_ 0)) (<= arg2_LSBRCK_2_RSBRCK_ 1)) (or ?v_2 (= arg2_LSBRCK_2_RSBRCK_ 1))) (or ARG2_LSBRCK_2_RSBRCK_ (= arg2_LSBRCK_2_RSBRCK_ 0))) (>= arg2_LSBRCK_3_RSBRCK_ 0)) (<= arg2_LSBRCK_3_RSBRCK_ 1)) (or ?v_3 (= arg2_LSBRCK_3_RSBRCK_ 1))) (or ARG2_LSBRCK_3_RSBRCK_ (= arg2_LSBRCK_3_RSBRCK_ 0))) (>= arg2_LSBRCK_4_RSBRCK_ 0)) (<= arg2_LSBRCK_4_RSBRCK_ 1)) (or ?v_4 (= arg2_LSBRCK_4_RSBRCK_ 1))) (or ARG2_LSBRCK_4_RSBRCK_ (= arg2_LSBRCK_4_RSBRCK_ 0))) (>= arg2_LSBRCK_5_RSBRCK_ 0)) (<= arg2_LSBRCK_5_RSBRCK_ 1)) (or ?v_5 (= arg2_LSBRCK_5_RSBRCK_ 1))) (or ARG2_LSBRCK_5_RSBRCK_ (= arg2_LSBRCK_5_RSBRCK_ 0))) (>= arg2_LSBRCK_6_RSBRCK_ 0)) (<= arg2_LSBRCK_6_RSBRCK_ 1)) (or ?v_6 (= arg2_LSBRCK_6_RSBRCK_ 1))) (or ARG2_LSBRCK_6_RSBRCK_ (= arg2_LSBRCK_6_RSBRCK_ 0))) (>= arg2_LSBRCK_7_RSBRCK_ 0)) (<= arg2_LSBRCK_7_RSBRCK_ 1)) (or ?v_7 (= arg2_LSBRCK_7_RSBRCK_ 1))) (or ARG2_LSBRCK_7_RSBRCK_ (= arg2_LSBRCK_7_RSBRCK_ 0))) (>= arg2_LSBRCK_8_RSBRCK_ 0)) (<= arg2_LSBRCK_8_RSBRCK_ 1)) (or ?v_8 (= arg2_LSBRCK_8_RSBRCK_ 1))) (or ARG2_LSBRCK_8_RSBRCK_ (= arg2_LSBRCK_8_RSBRCK_ 0))) (>= arg2_LSBRCK_9_RSBRCK_ 0)) (<= arg2_LSBRCK_9_RSBRCK_ 1)) (or ?v_9 (= arg2_LSBRCK_9_RSBRCK_ 1))) (or ARG2_LSBRCK_9_RSBRCK_ (= arg2_LSBRCK_9_RSBRCK_ 0))) (>= arg2_LSBRCK_10_RSBRCK_ 0)) (<= arg2_LSBRCK_10_RSBRCK_ 1)) (or ?v_10 (= arg2_LSBRCK_10_RSBRCK_ 1))) (or ARG2_LSBRCK_10_RSBRCK_ (= arg2_LSBRCK_10_RSBRCK_ 0))) (>= arg2_LSBRCK_11_RSBRCK_ 0)) (<= arg2_LSBRCK_11_RSBRCK_ 1)) (or ?v_11 (= arg2_LSBRCK_11_RSBRCK_ 1))) (or ARG2_LSBRCK_11_RSBRCK_ (= arg2_LSBRCK_11_RSBRCK_ 0))) (>= arg2_LSBRCK_12_RSBRCK_ 0)) (<= arg2_LSBRCK_12_RSBRCK_ 1)) (or ?v_12 (= arg2_LSBRCK_12_RSBRCK_ 1))) (or ARG2_LSBRCK_12_RSBRCK_ (= arg2_LSBRCK_12_RSBRCK_ 0))) (>= arg2_LSBRCK_13_RSBRCK_ 0)) (<= arg2_LSBRCK_13_RSBRCK_ 1)) (or ?v_13 (= arg2_LSBRCK_13_RSBRCK_ 1))) (or ARG2_LSBRCK_13_RSBRCK_ (= arg2_LSBRCK_13_RSBRCK_ 0))) (>= arg2_LSBRCK_14_RSBRCK_ 0)) (<= arg2_LSBRCK_14_RSBRCK_ 1)) (or ?v_14 (= arg2_LSBRCK_14_RSBRCK_ 1))) (or ARG2_LSBRCK_14_RSBRCK_ (= arg2_LSBRCK_14_RSBRCK_ 0))) (>= arg2_LSBRCK_15_RSBRCK_ 0)) (<= arg2_LSBRCK_15_RSBRCK_ 1)) (or ?v_15 (= arg2_LSBRCK_15_RSBRCK_ 1))) (or ARG2_LSBRCK_15_RSBRCK_ (= arg2_LSBRCK_15_RSBRCK_ 0))) (>= mul_sum_LSBRCK_0_RSBRCK_ 0)) (<= mul_sum_LSBRCK_0_RSBRCK_ 65535)) (>= arg1 0)) (<= arg1 65535)) (or ?v_0 (= mul_sum_LSBRCK_0_RSBRCK_ arg1))) (or ARG2_LSBRCK_0_RSBRCK_ (= mul_sum_LSBRCK_0_RSBRCK_ 0))) (>= mul_sum_LSBRCK_1_RSBRCK_ 0)) (<= mul_sum_LSBRCK_1_RSBRCK_ 65535)) (or ?v_1 (= mul_sum_LSBRCK_1_RSBRCK_ arg1))) (or ARG2_LSBRCK_1_RSBRCK_ (= mul_sum_LSBRCK_1_RSBRCK_ 0))) (>= mul_sum_LSBRCK_2_RSBRCK_ 0)) (<= mul_sum_LSBRCK_2_RSBRCK_ 65535)) (or ?v_2 (= mul_sum_LSBRCK_2_RSBRCK_ arg1))) (or ARG2_LSBRCK_2_RSBRCK_ (= mul_sum_LSBRCK_2_RSBRCK_ 0))) (>= mul_sum_LSBRCK_3_RSBRCK_ 0)) (<= mul_sum_LSBRCK_3_RSBRCK_ 65535)) (or ?v_3 (= mul_sum_LSBRCK_3_RSBRCK_ arg1))) (or ARG2_LSBRCK_3_RSBRCK_ (= mul_sum_LSBRCK_3_RSBRCK_ 0))) (>= mul_sum_LSBRCK_4_RSBRCK_ 0)) (<= mul_sum_LSBRCK_4_RSBRCK_ 65535)) (or ?v_4 (= mul_sum_LSBRCK_4_RSBRCK_ arg1))) (or ARG2_LSBRCK_4_RSBRCK_ (= mul_sum_LSBRCK_4_RSBRCK_ 0))) (>= mul_sum_LSBRCK_5_RSBRCK_ 0)) (<= mul_sum_LSBRCK_5_RSBRCK_ 65535)) (or ?v_5 (= mul_sum_LSBRCK_5_RSBRCK_ arg1))) (or ARG2_LSBRCK_5_RSBRCK_ (= mul_sum_LSBRCK_5_RSBRCK_ 0))) (>= mul_sum_LSBRCK_6_RSBRCK_ 0)) (<= mul_sum_LSBRCK_6_RSBRCK_ 65535)) (or ?v_6 (= mul_sum_LSBRCK_6_RSBRCK_ arg1))) (or ARG2_LSBRCK_6_RSBRCK_ (= mul_sum_LSBRCK_6_RSBRCK_ 0))) (>= mul_sum_LSBRCK_7_RSBRCK_ 0)) (<= mul_sum_LSBRCK_7_RSBRCK_ 65535)) (or ?v_7 (= mul_sum_LSBRCK_7_RSBRCK_ arg1))) (or ARG2_LSBRCK_7_RSBRCK_ (= mul_sum_LSBRCK_7_RSBRCK_ 0))) (>= mul_sum_LSBRCK_8_RSBRCK_ 0)) (<= mul_sum_LSBRCK_8_RSBRCK_ 65535)) (or ?v_8 (= mul_sum_LSBRCK_8_RSBRCK_ arg1))) (or ARG2_LSBRCK_8_RSBRCK_ (= mul_sum_LSBRCK_8_RSBRCK_ 0))) (>= mul_sum_LSBRCK_9_RSBRCK_ 0)) (<= mul_sum_LSBRCK_9_RSBRCK_ 65535)) (or ?v_9 (= mul_sum_LSBRCK_9_RSBRCK_ arg1))) (or ARG2_LSBRCK_9_RSBRCK_ (= mul_sum_LSBRCK_9_RSBRCK_ 0))) (>= mul_sum_LSBRCK_10_RSBRCK_ 0)) (<= mul_sum_LSBRCK_10_RSBRCK_ 65535)) (or ?v_10 (= mul_sum_LSBRCK_10_RSBRCK_ arg1))) (or ARG2_LSBRCK_10_RSBRCK_ (= mul_sum_LSBRCK_10_RSBRCK_ 0))) (>= mul_sum_LSBRCK_11_RSBRCK_ 0)) (<= mul_sum_LSBRCK_11_RSBRCK_ 65535)) (or ?v_11 (= mul_sum_LSBRCK_11_RSBRCK_ arg1))) (or ARG2_LSBRCK_11_RSBRCK_ (= mul_sum_LSBRCK_11_RSBRCK_ 0))) (>= mul_sum_LSBRCK_12_RSBRCK_ 0)) (<= mul_sum_LSBRCK_12_RSBRCK_ 65535)) (or ?v_12 (= mul_sum_LSBRCK_12_RSBRCK_ arg1))) (or ARG2_LSBRCK_12_RSBRCK_ (= mul_sum_LSBRCK_12_RSBRCK_ 0))) (>= mul_sum_LSBRCK_13_RSBRCK_ 0)) (<= mul_sum_LSBRCK_13_RSBRCK_ 65535)) (or ?v_13 (= mul_sum_LSBRCK_13_RSBRCK_ arg1))) (or ARG2_LSBRCK_13_RSBRCK_ (= mul_sum_LSBRCK_13_RSBRCK_ 0))) (>= mul_sum_LSBRCK_14_RSBRCK_ 0)) (<= mul_sum_LSBRCK_14_RSBRCK_ 65535)) (or ?v_14 (= mul_sum_LSBRCK_14_RSBRCK_ arg1))) (or ARG2_LSBRCK_14_RSBRCK_ (= mul_sum_LSBRCK_14_RSBRCK_ 0))) (>= mul_sum_LSBRCK_15_RSBRCK_ 0)) (<= mul_sum_LSBRCK_15_RSBRCK_ 65535)) (or ?v_15 (= mul_sum_LSBRCK_15_RSBRCK_ arg1))) (or ARG2_LSBRCK_15_RSBRCK_ (= mul_sum_LSBRCK_15_RSBRCK_ 0))) (>= mul_sum 0)) (<= mul_sum 4294967295)) (= (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- (- mul_sum mul_sum_LSBRCK_0_RSBRCK_) (* 2 mul_sum_LSBRCK_1_RSBRCK_)) (* 4 mul_sum_LSBRCK_2_RSBRCK_)) (* 8 mul_sum_LSBRCK_3_RSBRCK_)) (* 16 mul_sum_LSBRCK_4_RSBRCK_)) (* 32 mul_sum_LSBRCK_5_RSBRCK_)) (* 64 mul_sum_LSBRCK_6_RSBRCK_)) (* 128 mul_sum_LSBRCK_7_RSBRCK_)) (* 256 mul_sum_LSBRCK_8_RSBRCK_)) (* 512 mul_sum_LSBRCK_9_RSBRCK_)) (* 1024 mul_sum_LSBRCK_10_RSBRCK_)) (* 2048 mul_sum_LSBRCK_11_RSBRCK_)) (* 4096 mul_sum_LSBRCK_12_RSBRCK_)) (* 8192 mul_sum_LSBRCK_13_RSBRCK_)) (* 16384 mul_sum_LSBRCK_14_RSBRCK_)) (* 32768 mul_sum_LSBRCK_15_RSBRCK_)) 0)) (>= mul 0)) (<= mul 4294967295)) (= mul mul_sum)) (= mul 4293001441))))
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
